Shavrukovのbimodal provability logic GR